Michael Shulman axiom of 2-choice

The following definition is due to Mathieu Dupont.

Definition

A regular 2-category $K$ satisfies the axiom of 2-choice if every eso from a groupoidal object to a discrete object admits a splitting.

Conjecture

A (2,1)-exact and countably-coherent 2-category $K$ satisfies the axiom of 2-choice iff 1. $gpd(K)$ has enough discretes and 1. $disc(K)$ satisfies the ordinary axiom of choice (with respect to regular epis).

The “if” direction is clearly true even without exactness: given an eso $X\to A$ where $A$ is discrete and $X$ is groupoidal, find an eso $G\to X$ where $G$ is discrete, and then split the composite $G\to A$. Conversely, since discrete objects are groupoidal, the axiom of 2-choice clearly implies the ordinary axiom of choice (“1-choice”) for $disc(K)$. So it remains only to prove that 2-choice implies the existence of enough discretes in $gpd(K)$.

The obvious approach is: given $X$, we construct its discrete reflection $X_{\le 0}$. Then by assumption, the eso $X\to X_{\le 0}$ admits a splitting $X_{\le 0}\to X$, which we would like to show is also eso. Since the discretization of $X\to X_{\le 0}$ is an isomorphism, so is the discretization of its splitting, so it would suffice to know that for a map $f$ in a (2,1)-exact (2,1)-category, if the discretization of $f$ is an isomorphism, then $f$ is eso.

This is true in a (2,1)-topos, by internal arguing in homotopy type theory; see sets cover.